A:Type, eq:EqDecider(A), f, g:a:A fp Top, x:A, z:Top.
f  g(x)?z ~ if x  dom(f) f(x)?z else g(x)?z fi 

latex

Definitions	f(x)?z, f  g, true, Unit, , b, P  Q, P & Q, x. t(x), Prop, True, Top, a:A fp B(a), EqDecider(T), if b t else f fi, A, P  Q, False, P  Q, {T}, b, t  T, x  dom(f), x:A. B(x)
Lemmas	fpf-dom wf, assert wf, fpf-join-dom, not functionality wrt iff, not wf, bnot wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, btrue wf, bool wf, fpf-join wf, fpf-join-ap-sq, deq wf, top wf, fpf wf